Lean 4 ログ

定義上(definitionally)等しいような変形だけを行うという制約付きの simp

assumption

code:memo

命題外延性の公理 propext

商型 Quot の構築 : 関数外延性 funext を含意する

選択原理 Classical.choice : 存在命題 Nonempty α からデータ a : α を生成する

propext, funext

setext

命題論理に帰着させる

Eq.reqOn

商型Quot

Quot.mk

Quot.sound

同値型がくっついた型クラス

Lean 4は、auto bound implicit arguments(自動束縛暗黙引数)という新機能をサポートしている。この機能により、compose のような関数をより便利に書くことができる。Leanが定義宣言の前提を処理するとき、まだ束縛されていない識別子が1文字の小文字かギリシャ文字であれば、それらが暗黙引数として自動的に追加される。この機能を使うと、 compose を次のように書くことができる。

code:lean.haskell

def compose (g : β → γ) (f : α → β) (x : α) : γ :=

g (f x)

-- {β : Sort u_1} → {γ : Sort u_2} → {α : Sort u_3} → (β → γ) → (α → β) → α → γ

しかし、ある関数の引数を暗黙の引数として宣言しておきながら、その引数を明示的に与えたいという状況に陥ることがある。 foo がそのような関数である場合、 @foo という表記は、すべての引数を明示的にした同じ関数を表す。

@をつけることで